$\forall$${\it es}$:ES, ${\it ff}$:FIFO, $p$:(E$\rightarrow\mathbb{P}$), $e$:E, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C.
\\[0ex](${\it ff}$.C $\subseteq$r Id)
\\[0ex]$\Rightarrow$ ($\forall$$i$, $j$:${\it ff}$.C, $e$:E. (${\it ff}$.S($i$,$j$,$e$)) $\Rightarrow$ (loc($e$) = $i$ $\in$ Id))
\\[0ex]$\Rightarrow$ [$e$: ${\it sndr}$ $--$$p$$\rightarrow$ ${\it rcvr}$]
\\[0ex]$\Rightarrow$ (loc($e$) = ${\it sndr}$ $\in$ Id)